

unsigned int* printtab(){
	int maxsize= 100;
	char *file = "input.cnf";
	FILE *fp=fopen(file,"r");
	char* line;
	line = (char*) malloc(maxsize * sizeof(char));
	int lits[4] = {0};
	unsigned int clause = 0;
	int i, j;
	int params[2] = {0};
	char str [20];
	
	fgets(line, maxsize, fp);
	while(line[0] != 'p'){
		fgets(line, maxsize, fp);
	}
	sscanf(line, "%s %s %d %d", str, str, &params[0], &params[1]);
	//printf("%d\n", params[1]);
	unsigned int* sortie = (unsigned int*) malloc(params[1]*sizeof(unsigned int));
	
	for(j = 0; j < params[1]; j++){
		clause=0;
		fscanf(fp, "%i %i %i %i", &lits[0], &lits[1], &lits[2], &lits[3]);
		//printf("%i %i %i\n", lits[0], lits[1], lits[2]);
		clause += (3 << 24);
		if(lits[0] < 0){
			clause += (1 << 23);
			lits[0] *= -1;
		}
		if(lits[1] < 0){
			clause += (1 << 15);
			lits[1] *= -1;
		}
		if(lits[2] < 0){
			clause += (1 << 7);
			lits[2] *= -1;
		}
		for (i = 0; i < 3; ++i){
			clause += (lits[i] << (16 - (8 * i)));
		}
		sortie[j]=clause;
	}
	fclose(fp);
	return sortie;
}
